﻿using System;
using System.Text;
using System.Collections.Generic;
using System.Linq;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using Microsoft.Pex.Framework;

namespace Benchmarks.McMinnThesisBen
{
    [TestClass, PexClass(typeof(Postcode))]    
    public class Postcode
    {
        static int  RESULT_ENTER_NEW_CHAR = 0;
        static int  RESULT_VALID = 1;
        static int  RESULT_INVALID = 2;

        bool pri_letter_1;
        bool pri_letter_2;
        bool pri_digit_1;
        bool pri_digit_2;
        bool space;

        bool sec_digit;
        bool sec_letter_1;
        bool sec_letter_2;
        bool end;

        public Postcode()
        {
            pri_letter_1 = true;
            pri_letter_2 = false;
            pri_digit_1 = false;
            pri_digit_2 = false;
            space = false;

            sec_digit = false;
            sec_letter_1 = false;
            sec_letter_2 = false;
            end = false;
        }

        private bool is_letter(int unicode_char)
        {
            if (unicode_char >= 65 && unicode_char <= 90)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        private bool is_digit(int unicode_char)
        {
            if (unicode_char >= 48 && unicode_char <= 57)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        private bool is_space(int unicode_char)
        {
            if (unicode_char == 32)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        private bool is_lf(int unicode_char)
        {
            if (unicode_char == 12)
            {
                return true;
            }
            else
            {
                return false;
            }
        }

        public int validate_uk_postcode(int unicode_char)
        {
            int result = RESULT_ENTER_NEW_CHAR;
            if (pri_letter_1)
            {
                if (!is_letter(unicode_char))
                {
                    result = RESULT_INVALID;
                }
                else
                {
                    pri_letter_2 = true;
                    pri_letter_1 = false;
                }
            }
            else if (pri_letter_2)
            {
                if (is_letter(unicode_char))
                {
                    pri_digit_1 = true;
                    pri_letter_2 = false;
                }
                else if (is_digit(unicode_char))
                {
                    pri_digit_2 = true;
                    pri_letter_2 = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            else if (pri_digit_1)
            {
                if (is_digit(unicode_char))
                {
                    pri_digit_2 = true;
                    pri_digit_1 = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }        
            }
            else if (pri_digit_2)
            {
                if (is_digit(unicode_char))
                {
                    space = true;
                    pri_digit_2 = false;
                }
                else if (is_space(unicode_char))
                {
                    sec_digit = true;
                    pri_digit_2 = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            else if (space)
            {
                if (is_space(unicode_char))
                {
                    sec_digit = true;
                    space = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            else if (sec_digit)
            {
                if (is_digit(unicode_char))
                {
                    sec_letter_1 = true;
                    sec_digit = false;
                }
                else if (is_letter(unicode_char))
                {
                    sec_letter_2 = true;
                    sec_digit = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            else if (sec_letter_1)
            {
                 if (is_letter(unicode_char))
                 {
                    sec_letter_2 = true;
                    sec_letter_1 = false;
                 }
                 else
                 {
                    result = RESULT_INVALID;
                 }
            }
            else if (sec_letter_2)
            {
                if (is_letter(unicode_char))
                {
                    end = true;
                    sec_letter_2 = false;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            else if (end)
            {
                if (is_lf(unicode_char))
                {
                    pri_letter_1 = true;
                    end = false;
                    result = RESULT_VALID;
                }
                else
                {
                    result = RESULT_INVALID;
                }
            }
            return result;
       }


        //README of running these test methods with Pex
        //For each METHODNAME, run with C:\pex\bin\Debug>Pex Benchmarks.dll /mf:METHODNAME
        // adding /fte outputs all generated tests

        //in run 11, it reaches {80, 80}  34/75 
        //seems fitness not working, need to debug more
        //[PexMethod(MaxRuns = 20, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]        
        //public void TestPostcodeFitness(int[] chars)
        //{
        //    TestPostcode(chars);
        //}

        //[PexMethod(MaxRuns = 20, MaxConditions = int.MaxValue, MaxRunsWithoutNewTests = int.MaxValue)]        
        //public void TestPostcodeDefault(int[] chars)
        //{
        //    TestPostcode(chars);
        //}

        //private void TestPostcode(int[] chars)
        //{
        //    PexAssume.IsTrue(chars != null);

        //    Postcode c = new Postcode();
        //    for (int i = 0; i <= (chars.Length - 1); i++)
        //        c.validate_uk_postcode(chars[i]);
        //}
    }
}
